(declare-fun a () String)
(declare-fun b () String)
(declare-fun c () String)
(declare-fun d () Int)
(declare-fun e () Int)
(declare-fun f () Int)
(declare-fun k () Int)
(declare-fun g () String)
(declare-fun h () String)
(declare-fun i () String)
(declare-fun j () String)
(assert (>= e k))
(assert (and (str.contains (str.replace b h (str.at b (str.len b))) "S") (= (str.contains j "R") (str.contains j "Q") (str.contains j "P") (str.contains (str.substr a (str.len g) (str.len (str.replace b h (str.at b (str.len b))))) "O") (str.contains (str.substr a (str.len g) (str.len (str.replace b h (str.at b (str.len b))))) "N") (str.contains (str.substr a (str.len g) (str.len (str.replace c i (str.at c (str.len c))))) "M") (str.contains (str.substr a (str.len g) (str.len (str.replace b h (str.at b (str.len b))))) "L") (str.contains (str.replace b h (str.at b (str.len b))) "K") (str.contains (str.substr a (str.len g) (str.len (str.replace b h (str.at b (str.len b))))) "J") false (str.contains (str.substr a (str.len g) (str.len (str.replace b h (str.at b (str.len b))))) "I") (str.contains (str.substr a 0 (str.len j)) "H") (str.contains (str.replace c i (str.at c 0)) "GF") (str.contains (str.substr a (str.len g) (str.len (str.replace b h (str.at b (str.len b))))) "E") (str.contains (str.substr a (str.len g) (str.len (str.replace b h (str.at b (str.len b))))) "C") (str.contains (str.substr a (str.len g) (str.len (str.replace b h (str.at b (str.len b))))) "B") (str.contains (str.substr a (str.len g) (str.len (str.replace b h (str.at b (str.len b))))) "A"))))
(assert (not (str.in_re h (str.to_re "+"))))
(assert (>= k f 0))
(assert (= (str.substr c 0 (str.len i)) (str.substr b 0 (str.len h))))
(assert (<= f d))
(assert (not (str.in_re (str.substr a 0 (str.len g)) (str.to_re "%"))))
(assert (= (str.substr b 0 (str.len h)) g))
(check-sat)
